λ 演算

概述

阿隆佐·邱奇在1930年代发明的形式系统，用函数抽象和应用来刻画计算的本质。尽管语法极简（只有变量、函数抽象和应用三种构造），λ 演算被证明与图灵机完全等价，是函数式编程语言的的理论基础。

关键内容

核心语法

λ 演算的语法只有三种构造： 1. 变量：x, y, z, ... 2. 函数抽象（Abstraction）：λx.M — 定义一个以 x 为参数、返回 M 的函数 3. 应用（Application）：M N — 将函数 M 应用于参数 N

尽管语法如此简单，λ 演算能够表达任何可计算函数。例如，自然数、布尔值、条件语句、递归等都可以在纯 λ 演算中编码。

在判定问题中的角色

1936年春，Church 使用 λ 演算证明了判定问题 (Entscheidungsproblem)的答案是否定的： - 首先定义"有效可计算性"为"λ可定义性" - 然后证明存在不可 λ 定义的函数 - 因此，不存在通用算法能判定一阶逻辑中任意命题的真假

但 λ 演算是一个高度抽象的形式系统，普通人很难从中看到"计算"的直观含义。这正是阿兰·图灵同年用图灵机独立解决同一问题的不可替代的价值所在。

与图灵机的等价性

Turing 在其论文附录中证明了一个重要的等价性结果：

定理：一个函数是图灵可计算的，当且仅当它是 λ 可定义的。

这意味着，尽管图灵机和 λ 演算在表面上看起来完全不同——一个是基于机器操作的模型，一个是基于函数变换的形式系统——它们所定义的"可计算性"概念却是完全相同的。

这一等价性，连同后来被证明的与 Godel 的一般递归函数、Post 的产生式系统、Markov 算法等多种计算模型的等价性，共同构成了Church-Turing 论题的经验基础。

对编程语言的深远影响

λ 演算不仅是理论工具，它直接塑造了现代编程语言： - Lisp（1958）：John McCarthy 直接基于 λ 演算设计 - Haskell、ML、OCaml：纯函数式语言，核心语义即 λ 演算 - 现代语言的函数特性：Python 的 lambda、JavaScript 的箭头函数、Java 的方法引用，都是 λ 抽象的工程体现 - 类型理论：Simply Typed λ Calculus、System F、依赖类型等，构成了现代类型系统的理论基础

来源

raw/books/计算机科学/01-turing-on-computable-numbers.md
raw/books/计算机科学/05-mccarthy-lisp.md — McCarthy 将 λ 演算引入 LISP 实践